b:. (b = (b))  False 

latex

ProofTree

Definitions	False, , A, s = t, t  T, tt, ff, , Void, x:AB(x), P  Q, P  Q, x:A  B(x), P & Q, P  Q, b, x:A. B(x), Type, b, p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, f(a), x f y, a < b, p  q, p  q, p q, , Unit, left + right
Lemmas	inconsistent-bool-eq2, inconsistent-bool-eq, iff functionality wrt iff, iff wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, bool wf, bfalse wf, btrue wf, false wf